p:FinProbSpace, A, B:p-open(p), s:(Outcome). s  p-union(A;B)  (s  A  s  B) 

latex

Definitions	left + right, P  Q, , , s = t, x:A  B(x), x:A. B(x), #$n, t  T, x:A. B(x), {i..j}, Outcome, {x:A| B(x)} , x:AB(x), Type, A  B, S  T, P & Q, i  j < k, suptype(S; T), <a, b>, f(a), (i = j), if b then t else f fi , FinProbSpace, P  Q, False, A, x.A(x), P  Q, P  Q, s  C, p-union(A;B), p-open(p), , b, b, , {T}, SQType(T), s ~ t, Unit
Lemmas	bool cases, eqtt to assert, bool sq, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bool wf, bnot wf, not wf, assert wf, finite-prob-space wf, ifthenelse wf, eq int wf, le wf, nat wf, p-outcome wf, int seg wf